Inference at * 2 1 1 1 1 
Iof proof for Lemma primrec add:



1. T : Type
2. n : 
3. 0 < n
4. m:, b:T, c:({0..((n - 1)+m)}TT).
4. primrec((n - 1)+m;b;c) = primrec(n - 1;primrec(m;b;c);i,t. c(i+m,t))
5. m : 
6. b : T
7. c : {0..(n+m)}TT
8. b' : T
9. primrec(m;b;c) = b'
10. primrec((n - 1)+m;b;c) = primrec(n - 1;b';i,t. c(i+m,t))
11. (n+m = 0)
12. (n = 0)
  c((n - 1)+m,primrec((n - 1)+m;b;c)) = c((n - 1)+m,primrec(n - 1;b';i,t. c(i+m,t))) 

latex

 by ((HypSubst (-3) 0) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n
C)) (first_tok SupInf:t) inil_term))) 

latex

C.

Definitions	, t  T,
Lemmas	le wf